$\forall$$T$:Type, $L$:$T$ List. 0$<\parallel$$L$$\parallel$ $\Rightarrow$ ($\exists$$x$:$T$, ${\it L'}$:$T$ List. $L$ $=$ (${\it L'}$ @ [$x$]))